Nuprl Lemma : append_assoc_sq
0,22
postcript
pdf
as
,
bs
,
cs
:Top List. ((
as
@
bs
) @
cs
) ~ (
as
@
bs
@
cs
)
latex
Definitions
Top
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
top
wf
origin
as, bs, cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) as, bs, cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) x:A. B(x)
T